Nuprl Definition : ma-decla
0,22
postcript
pdf
a
declared in
M
== locl(
a
)
dom(1of(2of(
M
)))
latex
clarification:
a
declared in
M
== fpf-dom(KindDeq; locl(
a
); 1of(2of(
M
)))
latex
Definitions
b
,
x
dom(
f
)
,
KindDeq
,
locl(
a
)
,
1of(
t
)
,
2of(
t
)
FDL editor aliases
ma-decla
origin
dom(1of(2of(M)))
dom(1of(2of(M)))
b dom(f)